Mathlib CI status (docs):

• ✅ Mathlib branch lean-pr-testing-3647 has successfully built against this PR. (2024-03-10 22:32:36) View Log
• ✅ Mathlib branch lean-pr-testing-3647 has successfully built against this PR. (2024-03-10 23:12:45) View Log
• ✅ Mathlib branch lean-pr-testing-3647 has successfully built against this PR. (2024-03-11 16:29:00) View Log

For future reference, here is some additional info on the motivation behind this PR. Alloy allow users to external (C) implementations to definitions via Lean code. This is done via metaprogramming utilities, but is essentially equivalent to a definition followed an attribute [extern] command. For example:

alloy c extern def myAdd (x y : UInt32) : UInt32 := {
  return x + y;
}

is essentially equivalent to:

noncomputable opaque myAdd (x y : UInt32) : UInt32
attribute [extern "alloy_myAdd"] myAdd
alloy c section
LEAN_EXPORT uint32_t alloy_myAdd ( uint32_t x , uint32_t y ) {
  return x + y;
}
end

Libraries which use Alloy may define functions that perform actions that are morally impure or memory-unsafe. Thus, the library creators would like to mark the definition unsafe. However, passing this unsafe through Alloy's macros results in a noncomputable unsafe definition, which Lean currently forbids. For instance, using the above example:

alloy c extern unsafe def myAdd (x y : UInt32) : UInt32

would produce:

noncomputable unsafe opaque myAdd (x y : UInt32) : UInt32

which is forbidden. The goal of this PR is to allow such a use case.

The use of noncomputable in the Alloy's definitions could be avoided by adding the @[extern] attribute to the definition when it is declared. However, this would require some special casing in Alloy, as it also wants to support providing implementations for already-existing definitions (e.g., constructors or projections). Thus, for consistency, it always produces the implementation separately from the definition.